FDL - Nuprl Definition : existse-between1

Nuprl Definition : existse-between1

0,22

[e1,e2).P(e) ==

e:E. e1

e & (e <loc e2) & P(e)

clarification:

existse-between1(es;e1;e2;e.P(e)) ==

e:es-E(es). es-le(es;e1;e) & es-locl(es; e; e2) & P(e)

Definitions x:A. B(x), E, A & B, P & Q, e e' , (e <loc e')

FDL editor aliases existse-between1

Definitions	x:A. B(x), E, A & B, P & Q, e e' , (e <loc e')
FDL editor aliases	existse-between1